\begin{tabbing}
q{-}sat{-}constraints($k$;$A$;$y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\parallel$$y$$\parallel$ = $k$ $\in$ $\mathbb{Z}$)\+
\\[0ex]c$\wedge$ \=l\_all($A$;:($\mathbb{Q}$ List)\+
\\[0ex]$\times$ (:$\mathbb{Z}$
\\[0ex]$\times$ ($\mathbb{Q}$ List));$a$.\=let $F$,$r$,$G$ = $a$ in \+
\\[0ex]if\= ($r$ =$_{0}$ 0)\+
\\[0ex]then q{-}linear($k$;$j$.$F$[$j$]?0;$y$) = q{-}linear($k$;$j$.$G$[$j$]?0;$y$) $\in$ $\mathbb{Q}$
\-\\[0ex]if\= ($r$ =$_{0}$ 1)\+
\\[0ex]then q{-}linear($k$;$j$.$F$[$j$]?0;$y$) $\leq$ q{-}linear($k$;$j$.$G$[$j$]?0;$y$)
\-\\[0ex]else q{-}linear($k$;$j$.$F$[$j$]?0;$y$) $<$ q{-}linear($k$;$j$.$G$[$j$]?0;$y$)
\\[0ex]fi )
\-\-\-
\end{tabbing}